A Flexible Proof Format for SMT: a Proposal
Identifieur interne : 002200 ( Main/Exploration ); précédent : 002199; suivant : 002201A Flexible Proof Format for SMT: a Proposal
Auteurs : Frédéric Besson [France] ; Pascal Fontaine [France] ; Laurent Théry [France]Source :
Abstract
The standard input format for Satisfiability Modulo Theories (SMT) solvers has now reached its second version and integrates many of the features useful for users to interact with their favourite SMT solver. However, although many SMT solvers do output proofs, no standardised proof format exists. We, here, propose for discussion at the PxTP Workshop a generic proof format in the SMT-LIB philosophy that is flexible enough to be easily recast for any SMT solver. The format is configurable so that the proof can be provided by the solver at the desired level of detail.
Url:
Affiliations:
- France
- Grand Est, Lorraine (région), Région Bretagne
- Lorient, Metz, Nancy, Rennes
- Université de Bretagne-Sud, Université de Lorraine, Université de Rennes 1, Université européenne de Bretagne
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 000192
- to stream Hal, to step Curation: 000192
- to stream Hal, to step Checkpoint: 001C63
- to stream Main, to step Merge: 002244
- to stream Main, to step Curation: 002200
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Flexible Proof Format for SMT: a Proposal</title><author><name sortKey="Besson, Frederic" sort="Besson, Frederic" uniqKey="Besson F" first="Frédéric" last="Besson">Frédéric Besson</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-88187" status="VALID"><idno type="RNSR">200918993K</idno><orgName>Software certification with semantic analysis</orgName><orgName type="acronym">CELTIQUE</orgName><desc><address><addrLine>Campus de Beaulieu 35042 Rennes cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/celtique</ref></desc><listRelation><relation active="#struct-419153" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-419365" type="direct"></relation><relation active="#struct-105128" type="indirect"></relation><relation active="#struct-105160" type="indirect"></relation><relation active="#struct-172265" type="indirect"></relation><relation active="#struct-247362" type="indirect"></relation><relation active="#struct-300812" type="indirect"></relation><relation name="- RENNES" active="#struct-301232" type="indirect"></relation><relation active="#struct-301262" type="indirect"></relation><relation name="UMR6074" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-419153" type="direct"><org type="laboratory" xml:id="struct-419153" status="VALID"><idno type="RNSR">198018249C</idno><orgName>Inria Rennes – Bretagne Atlantique </orgName><desc><address><addrLine>Campus de beaulieu35042 Rennes cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/rennes</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-419365" type="direct"><org type="department" xml:id="struct-419365" status="VALID"><orgName>LANGAGE ET GÉNIE LOGICIEL</orgName><orgName type="acronym">IRISA-D4</orgName><desc><address><country key="FR"></country></address><ref type="url">https://www.irisa.fr/fr/departements/d4-langage-genie-logiciel</ref></desc><listRelation><relation active="#struct-105128" type="direct"></relation><relation active="#struct-105160" type="indirect"></relation><relation active="#struct-172265" type="indirect"></relation><relation active="#struct-247362" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300812" type="indirect"></relation><relation name="- RENNES" active="#struct-301232" type="indirect"></relation><relation active="#struct-301262" type="indirect"></relation><relation name="UMR6074" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-105128" type="indirect"><org type="laboratory" xml:id="struct-105128" status="VALID"><idno type="IdRef">026386909</idno><idno type="RNSR">200012163A</idno><orgName>Institut de Recherche en Informatique et Systèmes Aléatoires</orgName><orgName type="acronym">IRISA</orgName><date type="start">2000</date><desc><address><addrLine>Avenue du général LeclercCampus de Beaulieu 35042 RENNES CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.irisa.fr</ref></desc><listRelation><relation active="#struct-105160" type="direct"></relation><relation active="#struct-172265" type="direct"></relation><relation active="#struct-247362" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300812" type="direct"></relation><relation name="- RENNES" active="#struct-301232" type="direct"></relation><relation active="#struct-301262" type="direct"></relation><relation name="UMR6074" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-105160" type="indirect"><org type="institution" xml:id="struct-105160" status="VALID"><orgName>Université de Rennes 1</orgName><orgName type="acronym">UR1</orgName><desc><address><addrLine>2 rue du Thabor - CS 46510 - 35065 Rennes cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-rennes1.fr/</ref></desc></org></tutelle><tutelle active="#struct-172265" type="indirect"><org type="institution" xml:id="struct-172265" status="VALID"><orgName>Université de Bretagne Sud</orgName><orgName type="acronym">UBS</orgName><desc><address><addrLine>BP 92116 - 56321 Lorient cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-ubs.fr/</ref></desc></org></tutelle><tutelle active="#struct-247362" type="indirect"><org type="institution" xml:id="struct-247362" status="VALID"><orgName>École normale supérieure - Rennes</orgName><orgName type="acronym">ENS Rennes</orgName><desc><address><addrLine>Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz</addrLine><country key="FR"></country></address><ref type="url">http://www.ens-rennes.fr</ref></desc></org></tutelle><tutelle active="#struct-300812" type="indirect"><org type="institution" xml:id="struct-300812" status="VALID"><orgName>SUPELEC</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="- RENNES" active="#struct-301232" type="indirect"><org type="institution" xml:id="struct-301232" status="VALID"><orgName>Institut National des Sciences Appliquées</orgName><orgName type="acronym">INSA</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-301262" type="indirect"><org type="institution" xml:id="struct-301262" status="VALID"><orgName>Télécom Bretagne</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6074" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Rennes</settlement><region type="region" nuts="2">Région Bretagne</region></placeName><orgName type="university">Université de Rennes 1</orgName><orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName><placeName><settlement type="city">Lorient</settlement><region type="region" nuts="2">Région Bretagne</region></placeName><orgName type="university">Université de Bretagne-Sud</orgName><orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName></affiliation></author><author><name sortKey="Fontaine, Pascal" sort="Fontaine, Pascal" uniqKey="Fontaine P" first="Pascal" last="Fontaine">Pascal Fontaine</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Thery, Laurent" sort="Thery, Laurent" uniqKey="Thery L" first="Laurent" last="Théry">Laurent Théry</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-3208" status="VALID"><idno type="RNSR">200618405J</idno><orgName>Mathematical, Reasoning and Software</orgName><orgName type="acronym">MARELLE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www-sop.inria.fr/marelle/</ref></desc><listRelation><relation active="#struct-34586" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-34586" type="direct"><org type="laboratory" xml:id="struct-34586" status="VALID"><idno type="RNSR">198318250R</idno><orgName>Inria Sophia Antipolis - Méditerranée </orgName><orgName type="acronym">CRISAM</orgName><desc><address><addrLine>2004 route des Lucioles BP 93 06902 Sophia Antipolis</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/sophia/</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-00642544</idno><idno type="halId">hal-00642544</idno><idno type="halUri">https://hal.inria.fr/hal-00642544</idno><idno type="url">https://hal.inria.fr/hal-00642544</idno><date when="2011-08-01">2011-08-01</date><idno type="wicri:Area/Hal/Corpus">000192</idno><idno type="wicri:Area/Hal/Curation">000192</idno><idno type="wicri:Area/Hal/Checkpoint">001C63</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">001C63</idno><idno type="wicri:Area/Main/Merge">002244</idno><idno type="wicri:Area/Main/Curation">002200</idno><idno type="wicri:Area/Main/Exploration">002200</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">A Flexible Proof Format for SMT: a Proposal</title><author><name sortKey="Besson, Frederic" sort="Besson, Frederic" uniqKey="Besson F" first="Frédéric" last="Besson">Frédéric Besson</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-88187" status="VALID"><idno type="RNSR">200918993K</idno><orgName>Software certification with semantic analysis</orgName><orgName type="acronym">CELTIQUE</orgName><desc><address><addrLine>Campus de Beaulieu 35042 Rennes cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/celtique</ref></desc><listRelation><relation active="#struct-419153" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-419365" type="direct"></relation><relation active="#struct-105128" type="indirect"></relation><relation active="#struct-105160" type="indirect"></relation><relation active="#struct-172265" type="indirect"></relation><relation active="#struct-247362" type="indirect"></relation><relation active="#struct-300812" type="indirect"></relation><relation name="- RENNES" active="#struct-301232" type="indirect"></relation><relation active="#struct-301262" type="indirect"></relation><relation name="UMR6074" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-419153" type="direct"><org type="laboratory" xml:id="struct-419153" status="VALID"><idno type="RNSR">198018249C</idno><orgName>Inria Rennes – Bretagne Atlantique </orgName><desc><address><addrLine>Campus de beaulieu35042 Rennes cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/rennes</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-419365" type="direct"><org type="department" xml:id="struct-419365" status="VALID"><orgName>LANGAGE ET GÉNIE LOGICIEL</orgName><orgName type="acronym">IRISA-D4</orgName><desc><address><country key="FR"></country></address><ref type="url">https://www.irisa.fr/fr/departements/d4-langage-genie-logiciel</ref></desc><listRelation><relation active="#struct-105128" type="direct"></relation><relation active="#struct-105160" type="indirect"></relation><relation active="#struct-172265" type="indirect"></relation><relation active="#struct-247362" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300812" type="indirect"></relation><relation name="- RENNES" active="#struct-301232" type="indirect"></relation><relation active="#struct-301262" type="indirect"></relation><relation name="UMR6074" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-105128" type="indirect"><org type="laboratory" xml:id="struct-105128" status="VALID"><idno type="IdRef">026386909</idno><idno type="RNSR">200012163A</idno><orgName>Institut de Recherche en Informatique et Systèmes Aléatoires</orgName><orgName type="acronym">IRISA</orgName><date type="start">2000</date><desc><address><addrLine>Avenue du général LeclercCampus de Beaulieu 35042 RENNES CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.irisa.fr</ref></desc><listRelation><relation active="#struct-105160" type="direct"></relation><relation active="#struct-172265" type="direct"></relation><relation active="#struct-247362" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300812" type="direct"></relation><relation name="- RENNES" active="#struct-301232" type="direct"></relation><relation active="#struct-301262" type="direct"></relation><relation name="UMR6074" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-105160" type="indirect"><org type="institution" xml:id="struct-105160" status="VALID"><orgName>Université de Rennes 1</orgName><orgName type="acronym">UR1</orgName><desc><address><addrLine>2 rue du Thabor - CS 46510 - 35065 Rennes cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-rennes1.fr/</ref></desc></org></tutelle><tutelle active="#struct-172265" type="indirect"><org type="institution" xml:id="struct-172265" status="VALID"><orgName>Université de Bretagne Sud</orgName><orgName type="acronym">UBS</orgName><desc><address><addrLine>BP 92116 - 56321 Lorient cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-ubs.fr/</ref></desc></org></tutelle><tutelle active="#struct-247362" type="indirect"><org type="institution" xml:id="struct-247362" status="VALID"><orgName>École normale supérieure - Rennes</orgName><orgName type="acronym">ENS Rennes</orgName><desc><address><addrLine>Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz</addrLine><country key="FR"></country></address><ref type="url">http://www.ens-rennes.fr</ref></desc></org></tutelle><tutelle active="#struct-300812" type="indirect"><org type="institution" xml:id="struct-300812" status="VALID"><orgName>SUPELEC</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="- RENNES" active="#struct-301232" type="indirect"><org type="institution" xml:id="struct-301232" status="VALID"><orgName>Institut National des Sciences Appliquées</orgName><orgName type="acronym">INSA</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-301262" type="indirect"><org type="institution" xml:id="struct-301262" status="VALID"><orgName>Télécom Bretagne</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6074" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Rennes</settlement><region type="region" nuts="2">Région Bretagne</region></placeName><orgName type="university">Université de Rennes 1</orgName><orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName><placeName><settlement type="city">Lorient</settlement><region type="region" nuts="2">Région Bretagne</region></placeName><orgName type="university">Université de Bretagne-Sud</orgName><orgName type="institution" wicri:auto="newGroup">Université européenne de Bretagne</orgName></affiliation></author><author><name sortKey="Fontaine, Pascal" sort="Fontaine, Pascal" uniqKey="Fontaine P" first="Pascal" last="Fontaine">Pascal Fontaine</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-107895" status="VALID"><idno type="RNSR">201020692C</idno><orgName>Modeling and Verification of Distributed Algorithms and Systems</orgName><orgName type="acronym">VERIDIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/veridis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="IdRef">02636817X</idno><idno type="ISNI">0000000122597504</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName></affiliation></author><author><name sortKey="Thery, Laurent" sort="Thery, Laurent" uniqKey="Thery L" first="Laurent" last="Théry">Laurent Théry</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-3208" status="VALID"><idno type="RNSR">200618405J</idno><orgName>Mathematical, Reasoning and Software</orgName><orgName type="acronym">MARELLE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www-sop.inria.fr/marelle/</ref></desc><listRelation><relation active="#struct-34586" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-34586" type="direct"><org type="laboratory" xml:id="struct-34586" status="VALID"><idno type="RNSR">198318250R</idno><orgName>Inria Sophia Antipolis - Méditerranée </orgName><orgName type="acronym">CRISAM</orgName><desc><address><addrLine>2004 route des Lucioles BP 93 06902 Sophia Antipolis</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/centre/sophia/</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">The standard input format for Satisfiability Modulo Theories (SMT) solvers has now reached its second version and integrates many of the features useful for users to interact with their favourite SMT solver. However, although many SMT solvers do output proofs, no standardised proof format exists. We, here, propose for discussion at the PxTP Workshop a generic proof format in the SMT-LIB philosophy that is flexible enough to be easily recast for any SMT solver. The format is configurable so that the proof can be provided by the solver at the desired level of detail.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li><li>Région Bretagne</li></region><settlement><li>Lorient</li><li>Metz</li><li>Nancy</li><li>Rennes</li></settlement><orgName><li>Université de Bretagne-Sud</li><li>Université de Lorraine</li><li>Université de Rennes 1</li><li>Université européenne de Bretagne</li></orgName></list><tree><country name="France"><region name="Région Bretagne"><name sortKey="Besson, Frederic" sort="Besson, Frederic" uniqKey="Besson F" first="Frédéric" last="Besson">Frédéric Besson</name></region><name sortKey="Fontaine, Pascal" sort="Fontaine, Pascal" uniqKey="Fontaine P" first="Pascal" last="Fontaine">Pascal Fontaine</name><name sortKey="Thery, Laurent" sort="Thery, Laurent" uniqKey="Thery L" first="Laurent" last="Théry">Laurent Théry</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002200 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 002200 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:hal-00642544
|texte= A Flexible Proof Format for SMT: a Proposal
}}
| This area was generated with Dilib version V0.6.33. |  |